import Mathlib.Probability.ConditionalProbability
import Mathlib.Tactic

open MeasureTheory
open scoped ENNReal ProbabilityTheory

namespace CNVSDependentCollusionFull

variable {Ω : Type*} [MeasurableSpace Ω]

/-- Evento generato da una variabile aleatoria booleana di compromissione. -/
def compromiseEvent
    (X : ℕ → Ω → Bool)
    (i : ℕ) : Set Ω :=
  {ω | X i ω = true}

/-- Evento: i primi `n` frammenti critici sono tutti compromessi. -/
def prefixEvent (C : ℕ → Set Ω) : ℕ → Set Ω
  | 0 => Set.univ
  | n + 1 => prefixEvent C n ∩ C n

/--
Modello misura-teorico di collusione dipendente.

Non assume indipendenza.
Ogni compromissione è una variabile aleatoria booleana.
La dipendenza è modellata tramite probabilità condizionata.
-/
structure DependentCollusionModel (μ : Measure Ω) where
  isProb : IsProbabilityMeasure μ

  m : ℕ

  compromised : ℕ → Ω → Bool

  compromised_measurable :
    ∀ i : ℕ, Measurable (compromised i)

  RecStar : Set Ω

  pComp : ℝ≥0∞

  hpComp_lt_one : pComp < 1

  rec_requires_all :
    RecStar ⊆ prefixEvent (compromiseEvent compromised) m

  chain_rule_step :
    ∀ i : ℕ,
      i < m →
        μ (prefixEvent (compromiseEvent compromised) (i + 1))
          =
        μ (prefixEvent (compromiseEvent compromised) i)
          *
        μ[compromiseEvent compromised i |
          prefixEvent (compromiseEvent compromised) i]

  conditional_compromise_bound :
    ∀ i : ℕ,
      i < m →
        μ[compromiseEvent compromised i |
          prefixEvent (compromiseEvent compromised) i]
          ≤ pComp

/--
Bound sui primi `m` frammenti critici.

Questo è il cuore dipendente:
usa chain rule + bound condizionato,
non indipendenza.
-/
theorem prefix_compromise_probability_bound
    {μ : Measure Ω}
    (M : DependentCollusionModel μ) :
    μ (prefixEvent (compromiseEvent M.compromised) M.m)
      ≤ M.pComp ^ M.m := by
  letI : IsProbabilityMeasure μ := M.isProb

  have h :
      ∀ n : ℕ,
        n ≤ M.m →
          μ (prefixEvent (compromiseEvent M.compromised) n)
            ≤ M.pComp ^ n := by
    intro n hn
    induction n with
    | zero =>
        simp [prefixEvent]
    | succ n ih =>
        have hn_lt : n < M.m := Nat.lt_of_succ_le hn
        calc
          μ (prefixEvent (compromiseEvent M.compromised) (n + 1))
              =
            μ (prefixEvent (compromiseEvent M.compromised) n)
              *
            μ[compromiseEvent M.compromised n |
              prefixEvent (compromiseEvent M.compromised) n] := by
                exact M.chain_rule_step n hn_lt
          _ ≤ M.pComp ^ n * M.pComp := by
                exact mul_le_mul'
                  (ih (Nat.le_trans (Nat.le_succ n) hn))
                  (M.conditional_compromise_bound n hn_lt)
          _ = M.pComp ^ (n + 1) := by
                rw [pow_succ]

  exact h M.m le_rfl

/--
Teorema dipendente completo:

Se la ricostruzione non autorizzata richiede tutti gli `m`
frammenti critici, e ogni compromissione condizionata è
uniformemente limitata da `pComp`, allora:

P(Rec*) ≤ pComp^m.
-/
theorem dependent_collusion_reconstruction_bound
    {μ : Measure Ω}
    (M : DependentCollusionModel μ) :
    μ M.RecStar ≤ M.pComp ^ M.m := by
  exact le_trans
    (measure_mono M.rec_requires_all)
    (prefix_compromise_probability_bound M)

end CNVSDependentCollusionFull